es:event_system{i:l}, e':es-E(es), P:({e:es-E(es)| loc(e) = loc(e')  Id} prop{i:l}).
e<e'.P(e)  prop{i:l} 

latex

Definitions	b, P  Q, False, A, t  T, x:A. B(x), P  Q, es-locl(es; e; e'), loc(e), Id, event_system{i:l}, es-E(es), prop{i:l}, x(s), A c B, x:A. B(x), e<e'.P(e)
Lemmas	es-locl wf, es-E wf, event system wf, Id wf, es-loc wf, es-loc-pred